| Definitions | s = t, t  T, x:A  B(x),  x:A. B(x), ES, Type, AbsInterface(A), WellFnd{i}(A;x,y.R(x;y)), E, e  loc e' , l1 l2, P   Q, x:A  B(x), left + right, f(a), x(s), {T}, let x,y = A in B(x;y), t.1,  x:A. B(x), P  Q, (e <loc e'), type List, es-interface-history(es;X;e), Dec(P), b | a, a ~ b, a b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), r s, r < s, q-rel(r;x), Outcome, (x l), l_disjoint(T;l1;l2), (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), EState(T), a:A fp B(a), Id,  , strong-subtype(A;B), EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M),  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e',  , constant_function(f;A;B), SWellFounded(R(x;y)),  , pred!(e;e'),   x,y. t(x;y), <a, b>,  A, pred(e), first(e), x. t(x), P & Q, Top, [], x.A(x), first(e),  b, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , loc(e), False, P  Q, P Q, lastchange(x;e), es-init(es;e), True, pred(e), Void, as @ bs, e  X, X(e), p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', b, p q, p q, p q, ff, tt,  ,  T |